COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	blocks[w86,jmc]		New blocks axioms fixing sneak
C00007 ENDMK
C⊗;
blocks[w86,jmc]		New blocks axioms fixing sneak

Here are five axioms that seem to solve the sneak disjunction problem
for the blocks world using ordinary circumscription.  ab aspect0 s
is very like your non-existence of situations whose preconditions
aren't met.  The solution is also similar to cancellation of
inheritance.  I'm hopeful that the solution can be adapted to the
problem posed by Hanks and McDermott.

∀x l s.¬ab aspect1(x,l,s) ⊃ loc(x,result(move(x,l),s)) = l

∀x l s. ab aspect1(x,l,s) ⊃ ab aspect0 result(move(x,l),s)

∀x l s. ab aspect0 s ⊃ ab aspect1(x,l,s)

∀e s.ab aspect0 s ⊃ ab aspect0 result(e,s)

∀x y l s.loc(y,s) = top x ⊃ ab aspect1(x,l,s)

Suppose now that blocks  A  and  B  are on the table, and we move  A
onto  B  and then try to move  B.  Without the second, third and fourth
axioms, we can minimize abnormality by having  ab aspect1(A,top B,S0)
and  A  not movable on top of  B, so that  B  is movable in
result(move(A,top B),S0).  With these axioms, whenever  ab aspect1(A,top B,S0)
is true, ab aspect1(B,y,result(move(A,top B),S0))  will also be true, so
the unwanted solution of the original circumscription no longer minimizes  ab.

What do you think?
val
more on circumscription
Two remarks:

1. With regard to my generalization of pointwise; we might call it filtered
circumscription.  I said that when  f  is the identity function we get
pointwise circumscription; also when  f  is 1-1.  When  f  is constant
we get ordinary circumscription.  I still don't have any applications.

2. With regard to your example of the robot in the two rooms.  The
example is akin to my earlier remark about reasoning about the past
sometimes - in which case we want to give the present priority.  I
fear we are getting to cases in which the mental situation itself
is involved in deciding on circumscription priorities.  The same
physical rule determines the effect of a planned action and is
used to draw conclusions about the past from present information.
However, we want to give priority to the information antecedent
in our minds over possibilities that are deduced from it.  This is
what led me to start think about mental situation calculus,
so far without reaching a definite formalization.

val
filtered → fibered
If we call it fibered circumscription we have the analogy with
fiber spaces.  The range of  f  is the base space, and the
inverse image of a point is a fiber.

val
Two more ideas:

1. The reason why we can't get what we want in the blocks world
by ordinary circumscription is that the  ab's  we have been using
involve only single situations.  If our  ab's  or, more generally,
the ordering used involve a number of successive situations, I
think we'll be able to get what we want.

2. It seems to me that we should try to set up our axioms and
do our circumscriptions in such a way that we get a "definite
action system" in which all actions have definite preconditions
and effects by a single circumscription.

Neither of the above ideas is in a precise form yet.